Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		le(0,y)	→ true
2:		le(s(x),0)	→ false
3:		le(s(x),s(y))	→ le(x,y)
4:		minus(0,y)	→ 0
5:		minus(s(x),y)	→ if_minus(le(s(x),y),s(x),y)
6:		if_minus(true,s(x),y)	→ 0
7:		if_minus(false,s(x),y)	→ s(minus(x,y))
8:		quot(0,s(y))	→ 0
9:		quot(s(x),s(y))	→ s(quot(minus(x,y),s(y)))
10:		log(s(0))	→ 0
11:		log(s(s(x)))	→ s(log(s(quot(x,s(s(0))))))

There are 8 dependency pairs:


12:		LE(s(x),s(y))	→ LE(x,y)
13:		MINUS(s(x),y)	→ IF_MINUS(le(s(x),y),s(x),y)
14:		MINUS(s(x),y)	→ LE(s(x),y)
15:		IF_MINUS(false,s(x),y)	→ MINUS(x,y)
16:		QUOT(s(x),s(y))	→ QUOT(minus(x,y),s(y))
17:		QUOT(s(x),s(y))	→ MINUS(x,y)
18:		LOG(s(s(x)))	→ LOG(s(quot(x,s(s(0)))))
19:		LOG(s(s(x)))	→ QUOT(x,s(s(0)))

The approximated dependency graph contains 4 SCCs: {12}, {13,15}, {16} and {18}.

Consider the SCC {12}. There are no usable rules. By taking the AF π with π(LE) = 1 together with the lexicographic path order with empty precedence, rule 12 is strictly decreasing.

Consider the SCC {13,15}. The usable rules are {1-3}. By taking the AF π with π(le) = π(MINUS) = 1 and π(IF_MINUS) = 2 together with the lexicographic path order with precedence 0 ≻ true and s ≻ false, rule 13 is weakly decreasing and the rules in {1-3,15} are strictly decreasing.

Consider the SCC {16}. The usable rules are {1-7}. By taking the AF π with π(le) = π(minus) = π(QUOT) = 1 and π(if_minus) = 2 together with the lexicographic path order with precedence s ≻ 0 ≻ true and s ≻ false, the rules in {4,5,7} are weakly decreasing and the rules in {1-3,6,16} are strictly decreasing.

Consider the SCC {18}. The usable rules are {1-9}. By taking the AF π with π(le) = π(LOG) = π(minus) = π(quot) = 1 and π(if_minus) = 2 together with the lexicographic path order with precedence s ≻ 0 ≻ true and s ≻ false, the rules in {4,5,7-9} are weakly decreasing and the rules in {1-3,6,18} are strictly decreasing.

Hence the TRS is terminating.

Tyrolean Termination Tool (0.29 seconds) --- May 4, 2006